1  /-
  2  Copyright (c) 2019 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau
  5  
  6  Ring-theoretic supplement of data.polynomial.
  7  
  8  Main result: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
  9  -/
 10  
 11  import data.polynomial data.mv_polynomial
src         └─────────────┘ └────────────────┘
 12  import ring_theory.subring
src         └─────────────────┘
 13  import ring_theory.ideals ring_theory.noetherian
src         └────────────────┘ └────────────────────┘
 14  
 15  noncomputable theory
 16  local attribute [instance, priority 100] classical.prop_decidable
id                                                             └─────┘
src                                                            └─────┘
typ                                                            └─────┘
 17  
 18  universes u v w
 19  
 20  namespace polynomial
 21  
 22  variables (R : Type u) [comm_ring R]
id                           └───────┘
src                          └───────┘
typ                          └───────┘
 23  
 24  /-- The `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n`. -/
 25  def degree_le (n : with_bot ℕ) : submodule R (polynomial R) :=
 26  ⨅ k : ℕ, ⨅ h : ↑k > n, (lcoeff R k).ker
 27  
 28  variable {R}
 29  
 30  theorem mem_degree_le {n : with_bot ℕ} {f : polynomial R} :
 31    f ∈ degree_le R n ↔ degree f ≤ n :=
 32  by simp only [degree_le, submodule.mem_infi, degree_le_iff_coeff_zero, linear_map.mem_ker]; refl
id                 └───────┘  └────────────────┘  └──────────────────────┘  └────────────────┘
src     └─────────┘└───────┘└┘└────────────────┘└┘└──────────────────────┘└┘└────────────────┘  └────
typ     └─────────┘└───────┘└┘└────────────────┘└┘└──────────────────────┘└┘└────────────────┘  └────
doc     └─────────┘└───────┘└┘                  └┘                        └┘                    └────
txt     └─────────┘         └┘                  └┘                        └┘                    └────
par     └─────────┘         └┘                  └┘                        └┘                    └────
pid         └──┘└┘         └┘                  └┘                        └┘                        
st                └───────────────────────────────────────────────────────────────────────────────────
 33  
src  
typ  
doc  
txt  
par  
pid  
st   
 34  theorem degree_le_mono {m n : with_bot ℕ} (H : m ≤ n) :
id                                 └──────┘          
src                                └──────┘          
typ                                └──────┘          
 35    degree_le R m ≤ degree_le R n :=
id     └───────┘    └───────┘  
src    └───────┘      └───────┘
typ    └───────┘    └───────┘  
doc    └───────┘       └───────┘
 36  λ f hf, mem_degree_le.2 (le_trans (mem_degree_le.1 hf) H)
id      └┘  └───────────┘   └──────┘  └───────────┘  └┘  
src          └───────────┘   └──────┘  └───────────┘
typ     └┘  └───────────┘   └──────┘  └───────────┘  └┘  
 37  
 38  theorem degree_le_eq_span_X_pow {n : ℕ} :
id                                        
src                                       
typ                                       
 39    degree_le R n = submodule.span R ↑((finset.range (n+1)).image (λ n, X^n) : finset (polynomial R)) :=
id     └───────┘    └────────────┘    └──────────┘     └───┘           └────┘  └────────┘ 
src    └───────┘      └────────────┘     └──────────┘      └───┘             └────┘  └────────┘
typ    └───────┘    └────────────┘    └──────────┘     └───┘           └────┘  └────────┘ 
doc    └───────┘       └────────────┘      └──────────┘       └───┘              └────┘  └────────┘
 40  begin
st   └─────
 41    apply le_antisymm,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
 42    { intros p hp, replace hp := mem_degree_le.1 hp,
id                                  └───────────┘   └┘
src      └─────────┘  └────────────┘└───────────┘└─┘
typ      └─────────┘  └────────────┘└───────────┘└─┘└┘
doc      └─────────┘  └────────────┘             └─┘
txt      └─────────┘  └────────────┘             └─┘
par      └─────────┘  └────────────┘             └─┘
pid            └───┘         └─┘└─┘             └─┘
st   ───┘└─────────┘└────────────────────────────────┘└─
 43      rw [← finsupp.sum_single p, finsupp.sum, submodule.mem_coe],
id             └────────────────┘   └─────────┘  └───────────────┘
src      └────┘└────────────────┘ └┘└─────────┘└┘└───────────────┘
typ      └────┘└────────────────┘└┘└─────────┘└┘└───────────────┘
doc      └────┘                   └┘└─────────┘└┘                 
txt      └────┘                   └┘           └┘                 
par      └────┘                   └┘           └┘                 
pid        └──┘                   └┘           └┘                 
st   ─────────────────────────────┘└───────────┘└─────────────────┘└──
 44      refine submodule.sum_mem _ (λ k hk, _),
id              └───────────────┘
src      └─────┘└───────────────┘└─┘  └───────┘
typ      └─────┘└───────────────┘└─┘  └───────┘
doc      └─────┘                 └─┘  └───────┘
txt      └─────┘                 └─┘  └───────┘
par      └─────┘                 └─┘  └───────┘
pid                             └─┘  └───────┘
st   ─────────────────────────────────────────┘└─
 45      have := with_bot.coe_le_coe.1 (finset.sup_le_iff.1 hp k hk),
id               └─────────────────┘    └───────────────┘   └┘  └┘
src      └──────┘└─────────────────┘└─┘ └───────────────┘└─┘     
typ      └──────┘└─────────────────┘└─┘ └───────────────┘└─┘└┘└┘
doc      └──────┘                   └─┘                  └─┘     
txt      └──────┘                   └─┘                  └─┘     
par      └──────┘                   └─┘                  └─┘     
pid      └───┘└─┘                   └─┘                  └─┘     
st   ──────────────────────────────────────────────────────────────┘└─
 46      rw [single_eq_C_mul_X, C_mul'],
id           └───────────────┘  └────┘
src      └──┘└───────────────┘└┘└────┘
typ      └──┘└───────────────┘└┘└────┘
doc      └──┘                 └┘      
txt      └──┘                 └┘      
par      └──┘                 └┘      
pid        └┘                 └┘      
st   ────────────────────────┘└──────┘└──
 47      refine submodule.smul_mem _ _ (submodule.subset_span $ finset.mem_coe.2 $
id              └────────────────┘      └───────────────────┘   └────────────┘
src      └─────┘└────────────────┘└───┘ └───────────────────┘ └────────────┘└─┘ 
typ      └─────┘└────────────────┘└───┘ └───────────────────┘ └────────────┘└─┘ 
doc      └─────┘                  └───┘                                     └─┘ 
txt      └─────┘                  └───┘                                     └─┘ 
par      └─────┘                  └───┘                                     └─┘ 
pid                              └───┘                                     └─┘ 
st   ──────────────────────────────────────────────────────────────────────────────
 48        finset.mem_image.2 ⟨_, finset.mem_range.2 (nat.lt_succ_of_le this), rfl⟩) },
id         └──────────────┘       └──────────────┘    └───────────────┘ └──┘   └─┘
src  ─────┘└──────────────┘└─┘ └─┘└──────────────┘└─┘ └───────────────┘    └─┘└─┘└─┘
typ  ─────┘└──────────────┘└─┘ └─┘└──────────────┘└─┘ └───────────────┘└──┘└─┘└─┘└─┘
doc  ─────┘                └─┘ └─┘                └─┘                      └─┘   └─┘
txt  ─────┘                └─┘ └─┘                └─┘                      └─┘   └─┘
par  ─────┘                └─┘ └─┘                └─┘                      └─┘   └─┘
pid  ─────┘                └─┘ └─┘                └─┘                      └─┘   └┘
st   ───────────────────────────────────────────────────────────────────────────────┘└┘
 49    rw [submodule.span_le, finset.coe_image, set.image_subset_iff],
id         └───────────────┘  └──────────────┘  └──────────────────┘
src    └──┘└───────────────┘└┘└──────────────┘└┘└──────────────────┘
typ    └──┘└───────────────┘└┘└──────────────┘└┘└──────────────────┘
doc    └──┘                 └┘                └┘└──────────────────┘
txt    └──┘                 └┘                └┘                    
par    └──┘                 └┘                └┘                    
pid      └┘                 └┘                └┘                    
st   ──────────────────────┘└────────────────┘└────────────────────┘└──
 50    intros k hk, apply mem_degree_le.2,
id                        └───────────┘
src    └─────────┘  └────┘└───────────┘└┘
typ    └─────────┘  └────┘└───────────┘└┘
doc    └─────────┘  └────┘             └┘
txt    └─────────┘  └────┘             └┘
par    └─────────┘  └────┘             └┘
pid          └───┘                    └┘
st   ────────────┘└─────────────────────┘└─
 51    apply le_trans (degree_X_pow_le _) (with_bot.coe_le_coe.2 $ nat.le_of_lt_succ $ finset.mem_range.1 hk)
id           └──────┘  └─────────────┘     └─────────────────┘     └───────────────┘   └──────────────┘   └┘
src    └────┘└──────┘ └─────────────┘└──┘ └─────────────────┘└─┘ └───────────────┘ └──────────────┘└─┘  └┘
typ    └────┘└──────┘ └─────────────┘└──┘ └─────────────────┘└─┘ └───────────────┘ └──────────────┘└─┘└┘└┘
doc    └────┘                        └──┘                    └─┘                                   └─┘  └┘
txt    └────┘                        └──┘                    └─┘                                   └─┘  └┘
par    └────┘                        └──┘                    └─┘                                   └─┘  └┘
pid                                 └──┘                    └─┘                                   └─┘  
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────┘
 52  end
st   └─┘
 53  
 54  /-- Given a polynomial, return the polynomial whose coefficients are in
 55  the ring closure of the original coefficients. -/
 56  def restriction (p : polynomial R) : polynomial (ring.closure (↑p.frange : set R)) :=
id                        └────────┘     └────────┘  └──────────┘  └─────┘   └─┘ 
src                       └────────┘      └────────┘  └──────────┘   └─────┘   └─┘
typ                       └────────┘     └────────┘  └──────────┘  └─────┘   └─┘ 
doc                       └────────┘      └────────┘
 57  ⟨p.support, λ i, ⟨p.to_fun i,
id    └──────┘       └─────┘ 
src    └──────┘         └─────┘
typ   └──────┘       └─────┘ 
 58    if H : p.to_fun i = 0 then H.symm ▸ is_add_submonoid.zero_mem _
id     └┘     └─────┘          └───┘  └───────────────────────┘
src    └┘      └─────┘            └───┘  └───────────────────────┘
typ    └┘     └─────┘          └───┘  └───────────────────────┘
 59    else ring.subset_closure $ finsupp.mem_frange.2 ⟨H, i, rfl⟩⟩,
id          └─────────────────┘  └────────────────┘       └─┘
src         └─────────────────┘  └────────────────┘         └─┘
typ         └─────────────────┘  └────────────────┘       └─┘
 60  λ i, finsupp.mem_support_iff.trans (not_iff_not_of_iff ⟨λ H, subtype.eq H, subtype.mk.inj⟩)⟩
id       └─────────────────────┘└────┘  └────────────────┘      └────────┘   └────────────┘
src       └─────────────────────┘└────┘  └────────────────┘       └────────┘    └────────────┘
typ      └─────────────────────┘└────┘  └────────────────┘      └────────┘   └────────────┘
 61  
 62  @[simp] theorem coeff_restriction {p : polynomial R} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n := rfl
id                                          └────────┘             └───┘  └─────────┘      └───┘      └─┘
src                                         └────────┘              └───┘  └─────────┘        └───┘        └─┘
typ                                         └────────┘             └───┘  └─────────┘      └───┘      └─┘
doc    └──┘                                 └────────┘                └───┘  └─────────┘         └───┘
 63  
 64  @[simp] theorem coeff_restriction' {p : polynomial R} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n := rfl
id                                           └────────┘             └───┘  └─────────┘       └───┘      └─┘
src                                          └────────┘              └───┘  └─────────┘         └───┘        └─┘
typ                                          └────────┘             └───┘  └─────────┘       └───┘      └─┘
doc    └──┘                                  └────────┘               └───┘  └─────────┘           └───┘
 65  
 66  @[simp] theorem degree_restriction {p : polynomial R} : (restriction p).degree = p.degree := rfl
id                                           └────────┘      └─────────┘  └────┘   └─────┘    └─┘
src                                          └────────┘       └─────────┘   └────┘    └─────┘    └─┘
typ                                          └────────┘      └─────────┘  └────┘   └─────┘    └─┘
doc    └──┘                                  └────────┘       └─────────┘   └────┘     └─────┘
 67  
 68  @[simp] theorem nat_degree_restriction {p : polynomial R} : (restriction p).nat_degree = p.nat_degree := rfl
id                                               └────────┘      └─────────┘  └────────┘   └─────────┘    └─┘
src                                              └────────┘       └─────────┘   └────────┘    └─────────┘    └─┘
typ                                              └────────┘      └─────────┘  └────────┘   └─────────┘    └─┘
doc    └──┘                                      └────────┘       └─────────┘   └────────┘     └─────────┘
 69  
 70  @[simp] theorem monic_restriction {p : polynomial R} : monic (restriction p) ↔ monic p :=
id                                          └────────┘     └───┘  └─────────┘    └───┘ 
src                                         └────────┘      └───┘  └─────────┘     └───┘
typ                                         └────────┘     └───┘  └─────────┘    └───┘ 
doc    └──┘                                 └────────┘      └───┘  └─────────┘      └───┘
 71  ⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩
id        └───────┘ └─────────┘       └────────┘ 
src        └───────┘ └─────────┘         └────────┘
typ       └───────┘ └─────────┘       └────────┘ 
 72  
 73  @[simp] theorem restriction_zero : restriction (0 : polynomial R) = 0 := rfl
id                                      └─────────┘      └────────┘         └─┘
src                                     └─────────┘      └────────┘          └─┘
typ                                     └─────────┘      └────────┘         └─┘
doc    └──┘                             └─────────┘      └────────┘
 74  
 75  @[simp] theorem restriction_one : restriction (1 : polynomial R) = 1 :=
id                                     └─────────┘      └────────┘   
src                                    └─────────┘      └────────┘    
typ                                    └─────────┘      └────────┘   
doc    └──┘                            └─────────┘      └────────┘
 76  ext $ λ i, subtype.eq $ by rw [coeff_restriction', coeff_one, coeff_one]; split_ifs; refl
id   └─┘       └────────┘          └────────────────┘  └───────┘  └───────┘
src  └─┘        └────────┘      └──┘└────────────────┘└┘└───────┘└┘└───────┘  └───────┘  └────
typ  └─┘       └────────┘      └──┘└────────────────┘└┘└───────┘└┘└───────┘  └───────┘  └────
doc                             └──┘                  └┘         └┘           └───────┘  └────
txt                             └──┘                  └┘         └┘           └───────┘  └────
par                             └──┘                  └┘         └┘           └───────┘  └────
pid                               └┘                  └┘         └┘                          
st                             └─────────────────────┘└─────────┘└─────────┘└─────────────────
 77  
src  
typ  
doc  
txt  
par  
pid  
st   
 78  variables {S : Type v} [comm_ring S] {f : R → S} {x : S}
id                           └───────┘
src                          └───────┘
typ                          └───────┘
 79  
 80  theorem eval₂_restriction {p : polynomial R} :
id                                  └────────┘ 
src                                 └────────┘
typ                                 └────────┘ 
doc                                 └────────┘
 81    eval₂ f x p = eval₂ (f ∘ subtype.val) x p.restriction :=
id     └───┘     └───┘    └─────────┘   └──────────┘
src    └───┘        └───┘     └─────────┘     └──────────┘
typ    └───┘     └───┘    └─────────┘   └──────────┘
doc    └───┘         └───┘                      └──────────┘
 82  rfl
id   └─┘
src  └─┘
typ  └─┘
 83  
 84  section to_subring
 85  variables (p : polynomial R) (T : set R) [is_subring T]
id                  └────────┘         └─┘     └────────┘
src                 └────────┘         └─┘     └────────┘
typ                 └────────┘         └─┘     └────────┘
doc                 └────────┘                 └────────┘
 86  
 87  /-- Given a polynomial `p` and a subring `T` that contains the coefficients of `p`,
 88  return the corresponding polynomial whose coefficients are in `T. -/
 89  def to_subring (hp : ↑p.frange ⊆ T) : polynomial T :=
id                        └─────┘      └────────┘ 
src                        └─────┘       └────────┘
typ                       └─────┘      └────────┘ 
doc                                        └────────┘
 90  ⟨p.support, λ i, ⟨p.to_fun i,
id    └──────┘       └─────┘ 
src    └──────┘         └─────┘
typ   └──────┘       └─────┘ 
 91    if H : p.to_fun i = 0 then H.symm ▸ is_add_submonoid.zero_mem _
id     └┘     └─────┘          └───┘  └───────────────────────┘
src    └┘      └─────┘            └───┘  └───────────────────────┘
typ    └┘     └─────┘          └───┘  └───────────────────────┘
 92    else hp $ finsupp.mem_frange.2 ⟨H, i, rfl⟩⟩,
id          └┘  └────────────────┘       └─┘
src              └────────────────┘         └─┘
typ         └┘  └────────────────┘       └─┘
 93  λ i, finsupp.mem_support_iff.trans (not_iff_not_of_iff ⟨λ H, subtype.eq H, subtype.mk.inj⟩)⟩
id       └─────────────────────┘└────┘  └────────────────┘      └────────┘   └────────────┘
src       └─────────────────────┘└────┘  └────────────────┘       └────────┘    └────────────┘
typ      └─────────────────────┘└────┘  └────────────────┘      └────────┘   └────────────┘
 94  
 95  variables (hp : ↑p.frange ⊆ T)
id                    └─────┘ 
src                   └─────┘ 
typ                   └─────┘ 
 96  include hp
 97  
 98  @[simp] theorem coeff_to_subring {n : ℕ} : ↑(coeff (to_subring p T hp) n) = coeff p n := rfl
id                                              └───┘  └────────┘   └┘     └───┘      └─┘
src                                             └───┘  └────────┘             └───┘        └─┘
typ                                             └───┘  └────────┘   └┘     └───┘      └─┘
doc    └──┘                                       └───┘  └────────┘              └───┘
 99  
100  @[simp] theorem coeff_to_subring' {n : ℕ} : (coeff (to_subring p T hp) n).1 = coeff p n := rfl
id                                               └───┘  └────────┘   └┘      └───┘      └─┘
src                                              └───┘  └────────┘              └───┘        └─┘
typ                                              └───┘  └────────┘   └┘      └───┘      └─┘
doc    └──┘                                       └───┘  └────────┘                └───┘
101  
102  @[simp] theorem degree_to_subring : (to_subring p T hp).degree = p.degree := rfl
id                                        └────────┘   └┘ └────┘   └─────┘    └─┘
src                                       └────────┘        └────┘    └─────┘    └─┘
typ                                       └────────┘   └┘ └────┘   └─────┘    └─┘
doc    └──┘                               └────────┘        └────┘     └─────┘
103  
104  @[simp] theorem nat_degree_to_subring : (to_subring p T hp).nat_degree = p.nat_degree := rfl
id                                            └────────┘   └┘ └────────┘   └─────────┘    └─┘
src                                           └────────┘        └────────┘    └─────────┘    └─┘
typ                                           └────────┘   └┘ └────────┘   └─────────┘    └─┘
doc    └──┘                                   └────────┘        └────────┘     └─────────┘
105  
106  @[simp] theorem monic_to_subring : monic (to_subring p T hp) ↔ monic p :=
id                                      └───┘  └────────┘   └┘   └───┘ 
src                                     └───┘  └────────┘          └───┘
typ                                     └───┘  └────────┘   └┘   └───┘ 
doc    └──┘                             └───┘  └────────┘           └───┘
107  ⟨λ H, congr_arg subtype.val H, λ H, subtype.eq H⟩
id        └───────┘ └─────────┘       └────────┘ 
src        └───────┘ └─────────┘         └────────┘
typ       └───────┘ └─────────┘       └────────┘ 
108  
109  omit hp
110  
111  @[simp] theorem to_subring_zero : to_subring (0 : polynomial R) T (set.empty_subset _) = 0 := rfl
id                                     └────────┘      └────────┘     └──────────────┘          └─┘
src                                    └────────┘      └────────┘       └──────────────┘          └─┘
typ                                    └────────┘      └────────┘     └──────────────┘          └─┘
doc    └──┘                            └────────┘      └────────┘
112  
113  @[simp] theorem to_subring_one : to_subring (1 : polynomial R) T
id                                    └────────┘      └────────┘   
src                                   └────────┘      └────────┘
typ                                   └────────┘      └────────┘   
doc    └──┘                           └────────┘      └────────┘
114    (set.subset.trans (finset.coe_subset.2 finsupp.frange_single)
id      └──────────────┘  └───────────────┘  └───────────────────┘
src     └──────────────┘  └───────────────┘  └───────────────────┘
typ     └──────────────┘  └───────────────┘  └───────────────────┘
115      (set.singleton_subset_iff.2 (is_submonoid.one_mem _))) = 1 :=
id        └──────────────────────┘   └──────────────────┘      
src       └──────────────────────┘   └──────────────────┘      
typ       └──────────────────────┘   └──────────────────┘      
116  ext $ λ i, subtype.eq $ by rw [coeff_to_subring', coeff_one, coeff_one]; split_ifs; refl
id   └─┘       └────────┘          └───────────────┘  └───────┘  └───────┘
src  └─┘        └────────┘      └──┘└───────────────┘└┘└───────┘└┘└───────┘  └───────┘  └───┘
typ  └─┘       └────────┘      └──┘└───────────────┘└┘└───────┘└┘└───────┘  └───────┘  └───┘
doc                             └──┘                 └┘         └┘           └───────┘  └───┘
txt                             └──┘                 └┘         └┘           └───────┘  └───┘
par                             └──┘                 └┘         └┘           └───────┘  └───┘
pid                               └┘                 └┘         └┘                          
st                             └────────────────────┘└─────────┘└─────────┘└────────────────┘
117  end to_subring
118  
119  variables (T : set R) [is_subring T]
id                  └─┘     └────────┘
src                 └─┘     └────────┘
typ                 └─┘     └────────┘
doc                         └────────┘
120  
121  /-- Given a polynomial whose coefficients are in some subring, return
122  the corresponding polynomial whose coefificents are in the ambient ring. -/
123  def of_subring (p : polynomial T) : polynomial R :=
id                       └────────┘     └────────┘ 
src                      └────────┘      └────────┘
typ                      └────────┘     └────────┘ 
doc                      └────────┘      └────────┘
124  ⟨p.support, subtype.val ∘ p.to_fun,
id    └──────┘  └─────────┘  └─────┘
src    └──────┘  └─────────┘   └─────┘
typ   └──────┘  └─────────┘  └─────┘
125  λ n, finsupp.mem_support_iff.trans (not_iff_not_of_iff
id       └─────────────────────┘└────┘  └────────────────┘
src       └─────────────────────┘└────┘  └────────────────┘
typ      └─────────────────────┘└────┘  └────────────────┘
126    ⟨λ h, congr_arg subtype.val h, λ h, subtype.eq h⟩)⟩
id          └───────┘ └─────────┘       └────────┘ 
src          └───────┘ └─────────┘         └────────┘
typ         └───────┘ └─────────┘       └────────┘ 
127  
128  @[simp] theorem frange_of_subring {p : polynomial T} :
id                                          └────────┘ 
src                                         └────────┘
typ                                         └────────┘ 
doc    └──┘                                 └────────┘
129    ↑(p.of_subring T).frange ⊆ T :=
id      └─────────┘  └────┘   
src      └─────────┘   └────┘  
typ     └─────────┘  └────┘   
doc       └─────────┘
130  λ y H, let ⟨hy, x, hx⟩ := finsupp.mem_frange.1 H in hx ▸ (p.to_fun x).2
id        └─┘        └┘     └────────────────┘           └─────┘   
src                            └────────────────┘             └─────┘   
typ       └─┘        └┘     └────────────────┘           └─────┘   
131  
132  end polynomial
133  
134  variables {R : Type u} [comm_ring R]
id                          └───────┘
src                          └───────┘
typ                         └───────┘
135  
136  namespace ideal
137  open polynomial
138  
139  /-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
140  def of_polynomial (I : ideal (polynomial R)) : submodule R (polynomial R) :=
id                          └───┘  └────────┘      └───────┘   └────────┘ 
src                         └───┘  └────────┘       └───────┘    └────────┘
typ                         └───┘  └────────┘      └───────┘   └────────┘ 
doc                                └────────┘       └───────┘    └────────┘
141  { carrier := I.carrier,
id                └──────┘
src                └──────┘
typ               └──────┘
142    zero := I.zero_mem,
id             └───────┘
src             └───────┘
typ            └───────┘
143    add := λ _ _, I.add_mem,
id                 └──────┘
src                   └──────┘
typ                └──────┘
144    smul := λ c x H, by rw [← C_mul']; exact submodule.smul_mem _ _ H }
id                            └────┘         └────────────────┘     
src                        └────┘└────┘  └────┘└────────────────┘└───┘ 
typ                     └────┘└────┘  └────┘└────────────────┘└───┘
doc                        └────┘        └────┘                  └───┘ 
txt                        └────┘        └────┘                  └───┘ 
par                        └────┘        └────┘                  └───┘ 
pid                          └──┘                               └───┘ 
st                        └───────────┘└───────────────────────────────┘
145  
146  variables {I : ideal (polynomial R)}
id                  └───┘  └────────┘
src                 └───┘  └────────┘
typ                 └───┘  └────────┘
doc                        └────────┘
147  theorem mem_of_polynomial (x) : x ∈ I.of_polynomial ↔ x ∈ I := iff.rfl
id                                     └────────────┘        └─────┘
src                                      └────────────┘          └─────┘
typ                                    └────────────┘        └─────┘
doc                                       └────────────┘
148  variables (I)
149  
150  /-- Given an ideal `I` of `R[X]`, make the `R`-submodule of `I`
151  consisting of polynomials of degree ≤ `n`. -/
152  def degree_le (n : with_bot ℕ) : submodule R (polynomial R) :=
id                      └──────┘     └───────┘   └────────┘ 
src                     └──────┘     └───────┘    └────────┘
typ                     └──────┘     └───────┘   └────────┘ 
doc                                   └───────┘    └────────┘
153  degree_le R n ⊓ I.of_polynomial
id   └───────┘    └────────────┘
src  └───────┘       └────────────┘
typ  └───────┘    └────────────┘
doc  └───────┘        └────────────┘
154  
155  /-- Given an ideal `I` of `R[X]`, make the ideal in `R` of
156  leading coefficients of polynomials in `I` with degree ≤ `n`. -/
157  def leading_coeff_nth (n : ℕ) : ideal R :=
id                                  └───┘ 
src                                 └───┘
typ                                 └───┘ 
158  (I.degree_le n).map $ lcoeff R n
id    └────────┘  └─┘    └────┘  
src    └────────┘   └─┘    └────┘
typ   └────────┘  └─┘    └────┘  
doc    └────────┘   └─┘
159  
160  theorem mem_leading_coeff_nth (n : ℕ) (x) :
id                                      
src                                     
typ                                     
161    x ∈ I.leading_coeff_nth n ↔ ∃ p ∈ I, degree p ≤ n ∧ leading_coeff p = x :=
id       └────────────────┘        └────┘     └───────────┘   
src        └────────────────┘           └────┘       └───────────┘   
typ      └────────────────┘        └────┘     └───────────┘   
doc         └────────────────┘              └────┘         └───────────┘
162  begin
st   └─────
163    simp only [leading_coeff_nth, degree_le, submodule.mem_map, lcoeff_apply, submodule.mem_inf, mem_degree_le],
id                └───────────────┘  └───────┘  └───────────────┘  └──────────┘  └───────────────┘  └───────────┘
src    └─────────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────┘
typ    └─────────┘└───────────────┘└┘└───────┘└┘└───────────────┘└┘└──────────┘└┘└───────────────┘└┘└───────────┘
doc    └─────────┘└───────────────┘└┘└───────┘└┘                 └┘            └┘                 └┘             
txt    └─────────┘                 └┘         └┘                 └┘            └┘                 └┘             
par    └─────────┘                 └┘         └┘                 └┘            └┘                 └┘             
pid        └──┘└┘                 └┘         └┘                 └┘            └┘                 └┘             
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
164    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
165    { rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩,
src      └───────────────────────────┘
typ      └───────────────────────────┘
doc      └───────────────────────────┘
txt      └───────────────────────────┘
par      └───────────────────────────┘
pid            └─────────────────────┘
st   ───┘└───────────────────────────┘└─
166      cases lt_or_eq_of_le hpdeg with hpdeg hpdeg,
id             └────────────┘ └───┘
src      └────┘└────────────┘     └───────────────┘
typ      └────┘└────────────┘└───┘└───────────────┘
doc      └────┘                   └───────────────┘
txt      └────┘                   └───────────────┘
par      └────┘                   └───────────────┘
pid                              └───────────────┘
st   ──────────────────────────────────────────────┘└─
167      { refine ⟨0, I.zero_mem, lattice.bot_le, _⟩,
id                    └────────┘  └────────────┘
src        └─────┘ └─┘└────────┘└┘└────────────┘└──┘
typ        └─────┘ └─┘└────────┘└┘└────────────┘└──┘
doc        └─────┘ └─┘          └┘              └──┘
txt        └─────┘ └─┘          └┘              └──┘
par        └─────┘ └─┘          └┘              └──┘
pid               └─┘          └┘              └──┘
st   ─────┘└───────────────────────────────────────┘└─
168        rw [leading_coeff_zero, eq_comm],
id             └────────────────┘  └─────┘
src        └──┘└────────────────┘└┘└─────┘
typ        └──┘└────────────────┘└┘└─────┘
doc        └──┘                  └┘       
txt        └──┘                  └┘       
par        └──┘                  └┘       
pid          └┘                  └┘       
st   ───────────────────────────┘└───────┘└──
169        exact coeff_eq_zero_of_degree_lt hpdeg },
id               └────────────────────────┘ └───┘
src        └────┘└────────────────────────┘     
typ        └────┘└────────────────────────┘└───┘
doc        └────┘                               
txt        └────┘                               
par        └────┘                               
pid                                            
st   ────────────────────────────────────────────┘└┘
170      { refine ⟨p, hpI, le_of_eq hpdeg, _⟩,
id                   └─┘  └──────┘ └───┘
src        └─────┘  └┘   └┘└──────┘     └──┘
typ        └─────┘ └┘└─┘└┘└──────┘└───┘└──┘
doc        └─────┘  └┘   └┘             └──┘
txt        └─────┘  └┘   └┘             └──┘
par        └─────┘  └┘   └┘             └──┘
pid                └┘   └┘             └──┘
st   ───────────────────────────────────────┘└─
171        rw [leading_coeff, nat_degree, hpdeg], refl } },
id             └───────────┘  └────────┘  └───┘
src        └──┘└───────────┘└┘└────────┘└┘       └───┘
typ        └──┘└───────────┘└┘└────────┘└┘└───┘  └───┘
doc        └──┘└───────────┘└┘└────────┘└┘       └───┘
txt        └──┘             └┘          └┘       └───┘
par        └──┘             └┘          └┘       └───┘
pid          └┘             └┘          └┘           
st   ──────────────────────┘└──────────┘└─────┘└──────┘└──┘
172    { rintro ⟨p, hpI, hpdeg, rfl⟩,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid            └───────────────────┘
st   ──────────────────────────────┘└─
173      have : nat_degree p + (n - nat_degree p) = n,
id                                └────────┘    
src      └─────┘             └────────┘ └┘
typ      └─────┘             └────────┘└┘
doc      └─────┘               └────────┘ └┘ 
txt      └─────┘                          └┘ 
par      └─────┘                          └┘ 
pid      └───┘└┘                          └┘ 
st   ───────────────────────────────────────────────┘└─
174      { exact nat.add_sub_cancel' (nat_degree_le_of_degree_le hpdeg) },
id               └─────────────────┘  └────────────────────────┘ └───┘
src        └────┘└─────────────────┘ └────────────────────────┘     └┘
typ        └────┘└─────────────────┘ └────────────────────────┘└───┘└┘
doc        └────┘                                                   └┘
txt        └────┘                                                   └┘
par        └────┘                                                   └┘
pid                                                                
st   ─────┘└───────────────────────────────────────────────────────────┘└┘
175      refine ⟨p * X ^ (n - nat_degree p), ⟨_, I.mul_mem_right hpI⟩, _⟩,
id                        └────────┘        └─────────────┘ └─┘
src      └─────┘     └────────┘ └─┘ └─┘└─────────────┘   └───┘
typ      └─────┘    └────────┘└─┘ └─┘└─────────────┘└─┘└───┘
doc      └─────┘       └────────┘ └─┘ └─┘                  └───┘
txt      └─────┘                   └─┘ └─┘                  └───┘
par      └─────┘                   └─┘ └─┘                  └───┘
pid                               └─┘ └─┘                  └───┘
st   ───────────────────────────────────────────────────────────────────┘└─
176      { apply le_trans (degree_mul_le _ _) _,
id               └──────┘  └───────────┘
src        └────┘└──────┘ └───────────┘└─────┘
typ        └────┘└──────┘ └───────────┘└─────┘
doc        └────┘                      └─────┘
txt        └────┘                      └─────┘
par        └────┘                      └─────┘
pid                                   └─────┘
st   ─────┘└──────────────────────────────────┘└─
177        apply le_trans (add_le_add' (degree_le_nat_degree) (degree_X_pow_le _)) _,
id               └──────┘  └─────────┘  └──────────────────┘   └─────────────┘
src        └────┘└──────┘ └─────────┘ └──────────────────┘└┘ └─────────────┘└────┘
typ        └────┘└──────┘ └─────────┘ └──────────────────┘└┘ └─────────────┘└────┘
doc        └────┘                                         └┘                └────┘
txt        └────┘                                         └┘                └────┘
par        └────┘                                         └┘                └────┘
pid                                                      └┘                └────┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
178        rw [← with_bot.coe_add, this],
id               └──────────────┘  └──┘
src        └────┘└──────────────┘└┘    
typ        └────┘└──────────────┘└┘└──┘
doc        └────┘                └┘    
txt        └────┘                └┘    
par        └────┘                └┘    
pid          └──┘                └┘    
st   ───────────────────────────┘└────┘└──
179        exact le_refl _ },
id               └─────┘
src        └────┘└─────┘└─┘
typ        └────┘└─────┘└─┘
doc        └────┘       └─┘
txt        └────┘       └─┘
par        └────┘       └─┘
pid                    └┘
st   ─────────────────────┘└┘
180      { rw [leading_coeff, ← coeff_mul_X_pow p (n - nat_degree p), this] } }
id             └───────────┘    └─────────────┘       └────────┘    └──┘
src        └──┘└───────────┘└──┘└─────────────┘    └────────┘ └─┘    └┘
typ        └──┘└───────────┘└──┘└─────────────┘   └────────┘└─┘└──┘└┘
doc        └──┘└───────────┘└──┘                   └────────┘ └─┘    └┘
txt        └──┘             └──┘                              └─┘    └┘
par        └──┘             └──┘                              └─┘    └┘
pid          └┘             └──┘                              └─┘    
st   ──────────────────────┘└──────────────────────────────────────┘└────┘└───
181  end
st   ──┘
182  
183  theorem mem_leading_coeff_nth_zero (x) :
184    x ∈ I.leading_coeff_nth 0 ↔ C x ∈ I :=
id       └────────────────┘       
src        └────────────────┘       
typ      └────────────────┘       
doc         └────────────────┘     
185  (mem_leading_coeff_nth _ _ _).trans
id    └───────────────────┘       └───┘
src   └───────────────────┘       └───┘
typ   └───────────────────┘       └───┘
186  ⟨λ ⟨p, hpI, hpdeg, hpx⟩, by rwa [← hpx, leading_coeff,
id                                     └─┘  └───────────┘
src                              └─────┘   └┘└───────────┘└─
typ                             └─────┘└─┘└┘└───────────┘└─
doc                              └─────┘   └┘└───────────┘└─
txt                              └─────┘   └┘             └─
par                              └─────┘   └┘             └─
pid                                 └──┘   └┘             └─
st                              └─────────┘└─────────────┘└─
187    nat.eq_zero_of_le_zero (nat_degree_le_of_degree_le hpdeg),
id     └────────────────────┘  └────────────────────────┘ └───┘
src  ─┘└────────────────────┘ └────────────────────────┘     └──
typ  ─┘└────────────────────┘ └────────────────────────┘└───┘└──
doc  ─┘                                                      └──
txt  ─┘                                                      └──
par  ─┘                                                      └──
pid  ─┘                                                      └──
st   ──────────────────────────────────────────────────────────┘└─
188    ← eq_C_of_degree_le_zero hpdeg],
id       └────────────────────┘ └───┘
src  ───┘└────────────────────┘     
typ  ───┘└────────────────────┘└───┘
doc  ───┘                           
txt  ───┘                           
par  ───┘                           
pid  ───┘                           
st   ───────────────────────────────┘
189  λ hx, ⟨C x, hx, degree_C_le, leading_coeff_C x⟩⟩
id     └┘      └┘  └─────────┘  └─────────────┘ 
src                 └─────────┘  └─────────────┘
typ    └┘      └┘  └─────────┘  └─────────────┘ 
doc         
190  
191  theorem leading_coeff_nth_mono {m n : ℕ} (H : m ≤ n) :
id                                                  
src                                                 
typ                                                 
192    I.leading_coeff_nth m ≤ I.leading_coeff_nth n :=
id     └────────────────┘   └────────────────┘ 
src     └────────────────┘     └────────────────┘
typ    └────────────────┘   └────────────────┘ 
doc     └────────────────┘      └────────────────┘
193  begin
st   └─────
194    intros r hr,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
195    simp only [submodule.mem_coe, mem_leading_coeff_nth] at hr ⊢,
id                └───────────────┘  └───────────────────┘
src    └─────────┘└───────────────┘└┘└───────────────────┘└───────┘
typ    └─────────┘└───────────────┘└┘└───────────────────┘└───────┘
doc    └─────────┘                 └┘                     └───────┘
txt    └─────────┘                 └┘                     └───────┘
par    └─────────┘                 └┘                     └───────┘
pid        └──┘└┘                 └┘                     └─────┘
st   ─────────────────────────────────────────────────────────────┘└─
196    rcases hr with ⟨p, hpI, hpdeg, rfl⟩,
id            └┘
src    └─────┘  └────────────────────────┘
typ    └─────┘└┘└────────────────────────┘
doc    └─────┘  └────────────────────────┘
txt    └─────┘  └────────────────────────┘
par    └─────┘  └────────────────────────┘
pid            └────────────────────────┘
st   ────────────────────────────────────┘└─
197    refine ⟨p * X ^ (n - m), I.mul_mem_right hpI, _, leading_coeff_mul_X_pow⟩,
id                       └─────────────┘ └─┘     └─────────────────────┘
src    └─────┘     └─┘└─────────────┘   └───┘└─────────────────────┘
typ    └─────┘  └─┘└─────────────┘└─┘└───┘└─────────────────────┘
doc    └─────┘        └─┘                  └───┘                       
txt    └─────┘         └─┘                  └───┘                       
par    └─────┘         └─┘                  └───┘                       
pid                   └─┘                  └───┘                       
st   ──────────────────────────────────────────────────────────────────────────┘└─
198    refine le_trans (degree_mul_le _ _) _,
id            └──────┘  └───────────┘
src    └─────┘└──────┘ └───────────┘└─────┘
typ    └─────┘└──────┘ └───────────┘└─────┘
doc    └─────┘                      └─────┘
txt    └─────┘                      └─────┘
par    └─────┘                      └─────┘
pid                                └─────┘
st   ──────────────────────────────────────┘└─
199    refine le_trans (add_le_add' hpdeg (degree_X_pow_le _)) _,
id            └──────┘  └─────────┘ └───┘  └─────────────┘
src    └─────┘└──────┘ └─────────┘      └─────────────┘└────┘
typ    └─────┘└──────┘ └─────────┘└───┘ └─────────────┘└────┘
doc    └─────┘                                         └────┘
txt    └─────┘                                         └────┘
par    └─────┘                                         └────┘
pid                                                   └────┘
st   ──────────────────────────────────────────────────────────┘└─
200    rw [← with_bot.coe_add, nat.add_sub_cancel' H],
id           └──────────────┘  └─────────────────┘ 
src    └────┘└──────────────┘└┘└─────────────────┘ 
typ    └────┘└──────────────┘└┘└─────────────────┘
doc    └────┘                └┘                    
txt    └────┘                └┘                    
par    └────┘                └┘                    
pid      └──┘                └┘                    
st   ───────────────────────┘└─────────────────────┘└──
201    exact le_refl _
id           └─────┘
src    └────┘└─────┘└─┘
typ    └────┘└─────┘└─┘
doc    └────┘       └─┘
txt    └────┘       └─┘
par    └────┘       └─┘
pid                └┘
st   ─────────────────┘
202  end
st   └─┘
203  
204  /-- Given an ideal `I` in `R[X]`, make the ideal in `R` of the
205  leading coefficients in `I`. -/
206  def leading_coeff : ideal R :=
id                       └───┘ 
src                      └───┘
typ                      └───┘ 
207  ⨆ n : ℕ, I.leading_coeff_nth n
id         └────────────────┘ 
src         └────────────────┘
typ        └────────────────┘ 
doc          └────────────────┘
208  
209  theorem mem_leading_coeff (x) :
210    x ∈ I.leading_coeff ↔ ∃ p ∈ I, polynomial.leading_coeff p = x :=
id       └────────────┘       └──────────────────────┘   
src        └────────────┘         └──────────────────────┘   
typ      └────────────┘       └──────────────────────┘   
doc         └────────────┘            └──────────────────────┘
211  begin
st   └─────
212    rw [leading_coeff, submodule.mem_supr_of_directed],
id         └───────────┘  └────────────────────────────┘
src    └──┘└───────────┘└┘└────────────────────────────┘
typ    └──┘└───────────┘└┘└────────────────────────────┘
doc    └──┘└───────────┘└┘                              
txt    └──┘             └┘                              
par    └──┘             └┘                              
pid      └┘             └┘                              
st   ──────────────────┘└──────────────────────────────┘└──
213    simp only [mem_leading_coeff_nth],
id                └───────────────────┘
src    └─────────┘└───────────────────┘
typ    └─────────┘└───────────────────┘
doc    └─────────┘                     
txt    └─────────┘                     
par    └─────────┘                     
pid        └──┘└┘                     
st   ──────────────────────────────────┘└─
214    { split, { rintro ⟨i, p, hpI, hpdeg, rfl⟩, exact ⟨p, hpI, rfl⟩ },
id                                                         └─┘  └─┘
src      └───┘    └────────────────────────────┘  └────┘  └┘   └┘└─┘└┘
typ      └───┘    └────────────────────────────┘  └────┘ └┘└─┘└┘└─┘└┘
doc      └───┘    └────────────────────────────┘  └────┘  └┘   └┘   └┘
txt      └───┘    └────────────────────────────┘  └────┘  └┘   └┘   └┘
par      └───┘    └────────────────────────────┘  └────┘  └┘   └┘   └┘
pid                     └──────────────────────┘         └┘   └┘   
st   ───┘└───┘└──┘└────────────────────────────┘└────────────────────┘└┘
215      rintro ⟨p, hpI, rfl⟩, exact ⟨nat_degree p, p, hpI, degree_le_nat_degree, rfl⟩ },
id                                    └────────┘      └─┘  └──────────────────┘  └─┘
src      └──────────────────┘  └────┘ └────────┘ └┘ └┘   └┘└──────────────────┘└┘└─┘└┘
typ      └──────────────────┘  └────┘ └────────┘ └┘└┘└─┘└┘└──────────────────┘└┘└─┘└┘
doc      └──────────────────┘  └────┘ └────────┘ └┘ └┘   └┘                    └┘   └┘
txt      └──────────────────┘  └────┘            └┘ └┘   └┘                    └┘   └┘
par      └──────────────────┘  └────┘            └┘ └┘   └┘                    └┘   └┘
pid            └────────────┘                   └┘ └┘   └┘                    └┘   
st   ───────────────────────┘└────────────────────────────────────────────────────────┘└┘
216    { exact ⟨0⟩ },
src      └────┘ └─┘
typ      └────┘ └─┘
doc      └────┘ └─┘
txt      └────┘ └─┘
par      └────┘ └─┘
pid            └┘
st   ───┘└────────┘└┘
217    intros i j, exact ⟨i + j, I.leading_coeff_nth_mono (nat.le_add_right _ _),
id                                                      └──────────────┘
src    └────────┘  └────┘   └┘                         └──────────────┘└──────
typ    └────────┘  └────┘ └┘                         └──────────────┘└──────
doc    └────────┘  └────┘    └┘                                         └──────
txt    └────────┘  └────┘    └┘                                         └──────
par    └────────┘  └────┘    └┘                                         └──────
pid          └──┘           └┘                                         └──────
st   ───────────┘└────────────────────────────────────────────────────────────────
218      I.leading_coeff_nth_mono (nat.le_add_left _ _)⟩
id       └──────────────────────┘  └─────────────┘
src  ───┘└──────────────────────┘ └─────────────┘└─────┘
typ  ───┘└──────────────────────┘ └─────────────┘└─────┘
doc  ───┘                                        └─────┘
txt  ───┘                                        └─────┘
par  ───┘                                        └─────┘
pid  ───┘                                        └────┘
st   ───────────────────────────────────────────────────┘
219  end
st   └─┘
220  
221  theorem is_fg_degree_le [is_noetherian_ring R] (n : ℕ) :
id                            └────────────────┘        
src                           └────────────────┘         
typ                           └────────────────┘        
222    submodule.fg (I.degree_le n) :=
id     └──────────┘  └────────┘ 
src    └──────────┘   └────────┘
typ    └──────────┘  └────────┘ 
doc                   └────────┘
223  is_noetherian_submodule_left.1 (is_noetherian_of_fg_of_noetherian _
id   └──────────────────────────┘   └───────────────────────────────┘
src  └──────────────────────────┘   └───────────────────────────────┘
typ  └──────────────────────────┘   └───────────────────────────────┘
224    ⟨_, degree_le_eq_span_X_pow.symm⟩) _
id         └─────────────────────┘└───┘
src        └─────────────────────┘└───┘
typ        └─────────────────────┘└───┘
225  
226  end ideal
227  
228  /-- Hilbert basis theorem. -/
229  theorem is_noetherian_ring_polynomial [is_noetherian_ring R] : is_noetherian_ring (polynomial R) :=
id                                          └────────────────┘     └────────────────┘  └────────┘ 
src                                         └────────────────┘      └────────────────┘  └────────┘
typ                                         └────────────────┘     └────────────────┘  └────────┘ 
doc                                                                                     └────────┘
230  ⟨assume I : ideal (polynomial R),
id               └───┘  └────────┘ 
src              └───┘  └────────┘
typ              └───┘  └────────┘ 
doc                     └────────┘
231  let L := I.leading_coeff in
id           └────────────┘
src            └────────────┘
typ          └────────────┘
doc            └────────────┘
232  let M := well_founded.min (is_noetherian_iff_well_founded.1 (by apply_instance))
id           └──────────────┘  └────────────────────────────┘
src           └──────────────┘  └────────────────────────────┘      └────────────┘
typ          └──────────────┘  └────────────────────────────┘      └────────────┘
doc           └──────────────┘                                       └────────────┘
txt                                                                  └────────────┘
par                                                                  └────────────┘
st                                                                  └─────────────┘
233    (set.range I.leading_coeff_nth) ⟨_, ⟨0, rfl⟩⟩ in
id      └───────┘ └────────────────┘          └─┘
src     └───────┘  └────────────────┘          └─┘
typ     └───────┘ └────────────────┘          └─┘
doc     └───────┘  └────────────────┘
234  have hm : M ∈ set.range I.leading_coeff_nth := well_founded.min_mem _ _ _,
id               └───────┘ └────────────────┘    └──────────────────┘
src               └───────┘  └────────────────┘    └──────────────────┘
typ              └───────┘ └────────────────┘    └──────────────────┘
doc                └───────┘  └────────────────┘
235  let ⟨N, HN⟩ := hm, ⟨s, hs⟩ := I.is_fg_degree_le N in
id   └─┘    └┘     └┘     └┘     └──────────────┘
src                                 └──────────────┘
typ  └─┘    └┘     └┘     └┘     └──────────────┘
236  have hm2 : ∀ k, I.leading_coeff_nth k ≤ M := λ k, or.cases_on (le_or_lt k N)
id                  └────────────────┘           └─────────┘  └──────┘ 
src                   └────────────────┘              └─────────┘  └──────┘
typ                 └────────────────┘           └─────────┘  └──────┘ 
doc                   └────────────────┘
237    (λ h, HN ▸ I.leading_coeff_nth_mono h)
id              └─────────────────────┘ 
src               └─────────────────────┘
typ             └─────────────────────┘ 
238    (λ h x hx, classical.by_contradiction $ λ hxm,
id          └┘  └────────────────────────┘     └─┘
src               └────────────────────────┘
typ         └┘  └────────────────────────┘     └─┘
239      have ¬M < I.leading_coeff_nth k, by refine well_founded.not_lt_min
id              └────────────────┘             └─────────────────────┘
src               └────────────────┘       └─────┘└─────────────────────┘
typ             └────────────────┘      └─────┘└─────────────────────┘
doc                 └────────────────┘       └─────┘                       
txt                                          └─────┘                       
par                                          └─────┘                       
pid                                                                       
st                                          └───────────────────────────────
240        (well_founded_submodule_gt _ _) _ _ _; exact ⟨k, rfl⟩,
id          └───────────────────────┘                      └─┘
src  ─────┘ └───────────────────────┘└─────────┘  └────┘  └┘└─┘
typ  ─────┘ └───────────────────────┘└─────────┘  └────┘ └┘└─┘
doc  ─────┘                          └─────────┘  └────┘  └┘   
txt  ─────┘                          └─────────┘  └────┘  └┘   
par  ─────┘                          └─────────┘  └────┘  └┘   
pid  ─────┘                          └─────────┘         └┘   
st   ──────────────────────────────────────────────────────────┘
241      this ⟨HN ▸ I.leading_coeff_nth_mono (le_of_lt h), λ H, hxm (H hx)⟩),
id       └──┘      └─────────────────────┘  └──────┘        └─┘   └┘
src                 └─────────────────────┘  └──────┘
typ      └──┘      └─────────────────────┘  └──────┘        └─┘   └┘
242  have hs2 : ∀ {x}, x ∈ I.degree_le N → x ∈ ideal.span (↑s : set (polynomial R)),
id                      └────────┘       └────────┘      └─┘  └────────┘ 
src                        └────────┘        └────────┘      └─┘  └────────┘
typ                     └────────┘       └────────┘      └─┘  └────────┘ 
doc                         └────────┘                               └────────┘
243  from hs ▸ λ x hx, submodule.span_induction hx (λ _ hx, ideal.subset_span hx) (ideal.zero_mem _)
id               └┘  └──────────────────────┘ └┘     └┘  └───────────────┘ └┘   └────────────┘
src                   └──────────────────────┘             └───────────────┘      └────────────┘
typ              └┘  └──────────────────────┘ └┘     └┘  └───────────────┘ └┘   └────────────┘
doc                    └──────────────────────┘
244    (λ _ _, ideal.add_mem _) (λ c f hf, f.C_mul' c ▸ ideal.mul_mem_left _ hf),
id           └───────────┘         └┘  └─────┘   └────────────────┘   └┘
src            └───────────┘                └─────┘    └────────────────┘
typ          └───────────┘         └┘  └─────┘   └────────────────┘   └┘
245  ⟨s, le_antisymm (ideal.span_le.2 $ λ x hx, have x ∈ I.degree_le N, from hs ▸ submodule.subset_span hx, this.2) $ begin
id       └─────────┘  └───────────┘       └┘         └────────┘             └───────────────────┘ └┘  └──┘
src      └─────────┘  └───────────┘                     └────────┘             └───────────────────┘         
typ      └─────────┘  └───────────┘       └┘         └────────┘             └───────────────────┘ └┘  └──┘
doc                                                       └────────┘
st                                                                                                                    └─────
246    change I ≤ ideal.span ↑s,
id              └────────┘ 
src    └─────┘ └────────┘
typ    └─────┘└────────┘
doc    └─────┘            
txt    └─────┘            
par    └─────┘            
pid                      
st   ─────────────────────────┘└─
247    intros p hp, generalize hn : p.nat_degree = k,
id                                  └──────────┘
src    └─────────┘  └──────────────┘└──────────┘ 
typ    └─────────┘  └──────────────┘└──────────┘ 
doc    └─────────┘  └──────────────┘└──────────┘ 
txt    └─────────┘  └──────────────┘             
par    └─────────┘  └──────────────┘             
pid          └───┘            └─┘└┘             
st   ────────────┘└────────────────────────────────┘└─
248    induction k using nat.strong_induction_on with k ih generalizing p,
id               
src    └────────┘ └─────────────────────────────────────────────────────┘
typ    └────────┘└─────────────────────────────────────────────────────┘
doc    └────────┘ └─────────────────────────────────────────────────────┘
txt    └────────┘ └─────────────────────────────────────────────────────┘
par    └────────┘ └─────────────────────────────────────────────────────┘
pid              └────────────────────────────┘└────────┘└─────────────┘
st   ───────────────────────────────────────────────────────────────────┘└─
249    cases le_or_lt k N,
id           └──────┘  
src    └────┘└──────┘ 
typ    └────┘└──────┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ───────────────────┘└─
250    { subst k, refine hs2 ⟨polynomial.mem_degree_le.2
id                      └─┘  └──────────────────────┘
src      └────┘   └─────┘    └──────────────────────┘└──
typ      └────┘  └─────┘└─┘ └──────────────────────┘└──
doc      └────┘   └─────┘                            └──
txt      └────┘   └─────┘                            └──
par      └────┘   └─────┘                            └──
pid                                                └──
st   ───┘└─────┘└────────────────────────────────────────
251        (le_trans polynomial.degree_le_nat_degree $ with_bot.coe_le_coe.2 h), hp⟩ },
id          └──────┘ └─────────────────────────────┘   └─────────────────┘      └┘
src  ─────┘ └──────┘└─────────────────────────────┘ └─────────────────┘└─┘ └─┘  └┘
typ  ─────┘ └──────┘└─────────────────────────────┘ └─────────────────┘└─┘└─┘└┘└┘
doc  ─────┘                                                            └─┘ └─┘  └┘
txt  ─────┘                                                            └─┘ └─┘  └┘
par  ─────┘                                                            └─┘ └─┘  └┘
pid  ─────┘                                                            └─┘ └─┘  
st   ───────────────────────────────────────────────────────────────────────────────┘└┘
252    { have hp0 : p ≠ 0,
id                   
src      └─────────┘ └┘
typ      └─────────┘└┘
doc      └─────────┘  └┘
txt      └─────────┘  └┘
par      └─────────┘  └┘
pid      └──────┘└─┘  
st   ───────────────────┘└─
253      { rintro rfl, cases hn, exact nat.not_lt_zero _ h },
id                           └┘        └─────────────┘   
src        └────────┘  └────┘    └────┘└─────────────┘└─┘ 
typ        └────────┘  └────┘└┘  └────┘└─────────────┘└─┘
doc        └────────┘  └────┘    └────┘               └─┘ 
txt        └────────┘  └────┘    └────┘               └─┘ 
par        └────────┘  └────┘    └────┘               └─┘ 
pid              └──┘                               └─┘ 
st   ─────┘└────────┘└────────┘└──────────────────────────┘└┘
254      have : (0 : R) ≠ 1,
id                   
src      └─────┘ └──┘ └┘ └┘
typ      └─────┘ └──┘└┘ └┘
doc      └─────┘ └──┘ └┘ └┘
txt      └─────┘ └──┘ └┘ └┘
par      └─────┘ └──┘ └┘ └┘
pid      └───┘└┘ └──┘ └┘ 
st   ─────────────────────┘└─
255      { intro h, apply hp0, ext i, refine (mul_one _).symm.trans _,
id                                            └─────┘
src        └─────┘  └────┘     └───┘  └─────┘ └─────┘└──────────────┘
typ        └─────┘  └────┘     └───┘  └─────┘ └─────┘└──────────────┘
doc        └─────┘  └────┘     └───┘  └─────┘        └──────────────┘
txt        └─────┘  └────┘     └───┘  └─────┘        └──────────────┘
par        └─────┘  └────┘     └───┘  └─────┘        └──────────────┘
pid             └┘               └┘                └──────────────┘
st   ─────┘└─────┘└─────────┘└─────┘└───────────────────────────────┘└─
256        rw [← h, mul_zero], refl },
id                 └──────┘
src        └────┘ └┘└──────┘  └───┘
typ        └────┘└┘└──────┘  └───┘
doc        └────┘ └┘          └───┘
txt        └────┘ └┘          └───┘
par        └────┘ └┘          └───┘
pid          └──┘ └┘              
st   ────────────┘└────────┘└──────┘└┘
257      letI : nonzero_comm_ring R := { zero_ne_one := this,
id              └───────────────┘                      └──┘
src      └─────┘└───────────────┘ └──┘ └──────────────┘    └─
typ      └─────┘└───────────────┘└──┘ └──────────────┘└──┘└─
doc      └─────┘└───────────────┘ └──┘ └──────────────┘    └─
txt      └─────┘                  └──┘ └──────────────┘    └─
par      └─────┘                  └──┘ └──────────────┘    └─
pid          └┘                  └──┘ └──────────────┘    └─
st   ─────────────────────────────────────────────────────────
258        ..(infer_instance : comm_ring R) },
id            └────────────┘   └───────┘ 
src  ───────┘ └────────────┘└─┘└───────┘ └─┘
typ  ───────┘ └────────────┘└─┘└───────┘└─┘
doc  ───────┘ └────────────┘└─┘          └─┘
txt  ───────┘               └─┘          └─┘
par  ───────┘               └─┘          └─┘
pid  ───────┘               └─┘          └─┘
st   ───────────────────────────────────────┘└─
259      have : p.leading_coeff ∈ I.leading_coeff_nth N,
id              └─────────────┘  └─────────────────┘ 
src      └─────┘└─────────────┘└─────────────────┘
typ      └─────┘└─────────────┘└─────────────────┘
doc      └─────┘└─────────────┘ └─────────────────┘
txt      └─────┘                                   
par      └─────┘                                   
pid      └───┘└┘                                   
st   ─────────────────────────────────────────────────┘└─
260      { rw HN, exact hm2 k ((I.mem_leading_coeff_nth _ _).2
id            └┘        └─┘    └─────────────────────┘
src        └─┘    └────┘      └─────────────────────┘└───────
typ        └─┘└┘  └────┘└─┘  └─────────────────────┘└───────
doc        └─┘    └────┘                             └───────
txt        └─┘    └────┘                             └───────
par        └─┘    └────┘                             └───────
pid                                                └───────
st   ─────┘└───┘└──────────────────────────────────────────────
261          ⟨_, hp, hn ▸ polynomial.degree_le_nat_degree, rfl⟩) },
id               └┘  └┘  └─────────────────────────────┘  └─┘
src  ───────┘ └─┘  └┘  └─────────────────────────────┘└┘└─┘└─┘
typ  ───────┘ └─┘└┘└┘└┘└─────────────────────────────┘└┘└─┘└─┘
doc  ───────┘ └─┘  └┘                                  └┘   └─┘
txt  ───────┘ └─┘  └┘                                  └┘   └─┘
par  ───────┘ └─┘  └┘                                  └┘   └─┘
pid  ───────┘ └─┘  └┘                                  └┘   └┘
st   ───────────────────────────────────────────────────────────┘└┘
262      rw I.mem_leading_coeff_nth at this,
src      └─┘                       └──────┘
typ      └─┘└─────────────────────┘└──────┘
doc      └─┘                       └──────┘
txt      └─┘                       └──────┘
par      └─┘                       └──────┘
pid                               └──────┘
st   ─────────────────────────────────────┘└─
263      rcases this with ⟨q, hq, hdq, hlqp⟩,
id              └──┘
src      └─────┘    └──────────────────────┘
typ      └─────┘└──┘└──────────────────────┘
doc      └─────┘    └──────────────────────┘
txt      └─────┘    └──────────────────────┘
par      └─────┘    └──────────────────────┘
pid                └──────────────────────┘
st   ──────────────────────────────────────┘└─
264      have hq0 : q ≠ 0,
id                  
src      └─────────┘  └┘
typ      └─────────┘ └┘
doc      └─────────┘  └┘
txt      └─────────┘  └┘
par      └─────────┘  └┘
pid      └──────┘└─┘  
st   ───────────────────┘└─
265      { intro H, rw [← polynomial.leading_coeff_eq_zero] at H,
id                        └──────────────────────────────┘
src        └─────┘  └────┘└──────────────────────────────┘└────┘
typ        └─────┘  └────┘└──────────────────────────────┘└────┘
doc        └─────┘  └────┘                                └────┘
txt        └─────┘  └────┘                                └────┘
par        └─────┘  └────┘                                └────┘
pid             └┘    └──┘                                └───┘
st   ─────┘└─────┘└──────────────────────────────────────┘└───┘└─
266        rw [hlqp, polynomial.leading_coeff_eq_zero] at H, exact hp0 H },
id             └──┘  └──────────────────────────────┘              └─┘ 
src        └──┘    └┘└──────────────────────────────┘└────┘  └────┘    
typ        └──┘└──┘└┘└──────────────────────────────┘└────┘  └────┘└─┘
doc        └──┘    └┘                                └────┘  └────┘    
txt        └──┘    └┘                                └────┘  └────┘    
par        └──┘    └┘                                └────┘  └────┘    
pid          └┘    └┘                                └───┘           
st   ─────────────┘└────────────────────────────────┘└───┘└────────────┘└┘
267      have h1 : p.degree = (q * polynomial.X ^ (k - q.nat_degree)).degree,
id                 └──────┘       └──────────┘     └──────────┘
src      └────────┘└──────┘   └──────────┘  └──────────┘└───────┘
typ      └────────┘└──────┘   └──────────┘ └──────────┘└───────┘
doc      └────────┘└──────┘    └──────────┘    └──────────┘└───────┘
txt      └────────┘                                        └───────┘
par      └────────┘                                        └───────┘
pid      └─────┘└─┘                                        └──────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
268      { rw [polynomial.degree_mul_eq', polynomial.degree_X_pow],
id             └───────────────────────┘  └─────────────────────┘
src        └──┘└───────────────────────┘└┘└─────────────────────┘
typ        └──┘└───────────────────────┘└┘└─────────────────────┘
doc        └──┘                         └┘                       
txt        └──┘                         └┘                       
par        └──┘                         └┘                       
pid          └┘                         └┘                       
st   ─────┘└───────────────────────────┘└───────────────────────┘└──
269        rw [polynomial.degree_eq_nat_degree hp0, polynomial.degree_eq_nat_degree hq0],
id             └─────────────────────────────┘ └─┘  └─────────────────────────────┘ └─┘
src        └──┘└─────────────────────────────┘   └┘└─────────────────────────────┘   
typ        └──┘└─────────────────────────────┘└─┘└┘└─────────────────────────────┘└─┘
doc        └──┘                                  └┘                                  
txt        └──┘                                  └┘                                  
par        └──┘                                  └┘                                  
pid          └┘                                  └┘                                  
st   ────────────────────────────────────────────┘└───────────────────────────────────┘└──
270        rw [← with_bot.coe_add, nat.add_sub_cancel', hn],
id               └──────────────┘  └─────────────────┘  └┘
src        └────┘└──────────────┘└┘└─────────────────┘└┘  
typ        └────┘└──────────────┘└┘└─────────────────┘└┘└┘
doc        └────┘                └┘                   └┘  
txt        └────┘                └┘                   └┘  
par        └────┘                └┘                   └┘  
pid          └──┘                └┘                   └┘  
st   ───────────────────────────┘└───────────────────┘└──┘
271        { refine le_trans (polynomial.nat_degree_le_of_degree_le hdq) (le_of_lt h) },
st                                                                                    
272        rw [polynomial.leading_coeff_X_pow, mul_one],
273        exact mt polynomial.leading_coeff_eq_zero.1 hq0 },
st                                                         
274      have h2 : p.leading_coeff = (q * polynomial.X ^ (k - q.nat_degree)).leading_coeff,
275      { rw [← hlqp, polynomial.leading_coeff_mul_X_pow] },
src                                                      
typ                                                      
doc                                                      
txt                                                      
par                                                      
pid                                                      
st                                                        
276      have := polynomial.degree_sub_lt h1 hp0 h2,
277      rw [polynomial.degree_eq_nat_degree hp0] at this,
278      rw ← sub_add_cancel p (q * polynomial.X ^ (k - q.nat_degree)),
279      refine (ideal.span ↑s).add_mem _ ((ideal.span ↑s).mul_mem_right _),
280      { by_cases hpq : p - q * polynomial.X ^ (k - q.nat_degree) = 0,
281        { rw hpq, exact ideal.zero_mem _ },
st                                          
282        refine ih _ _ (I.sub_mem hp (I.mul_mem_right hq)) rfl,
283        rwa [polynomial.degree_eq_nat_degree hpq, with_bot.coe_lt_coe, hn] at this },
st                                                                                    
284      exact hs2 ⟨polynomial.mem_degree_le.2 hdq, hq⟩ }
st                                                      └─
285  end⟩⟩
st   ──┘
286  
287  theorem is_noetherian_ring_mv_polynomial_fin {n : ℕ} [is_noetherian_ring R] :
id                                                        └────────────────┘ 
src                                                       └────────────────┘
typ                                                       └────────────────┘ 
288    is_noetherian_ring (mv_polynomial (fin n) R) :=
id     └────────────────┘  └───────────┘  └─┘   
src    └────────────────┘  └───────────┘  └─┘
typ    └────────────────┘  └───────────┘  └─┘   
doc                        └───────────┘
289  begin
st   └─────
290    induction n with n ih,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
291    { exact is_noetherian_ring_of_ring_equiv R
id             └──────────────────────────────┘
src      └────┘└──────────────────────────────┘ 
typ      └────┘└──────────────────────────────┘ 
doc      └────┘                                 
txt      └────┘                                 
par      └────┘                                 
pid                                            
st   ───┘└────────────────────────────────────────
292        ((mv_polynomial.pempty_ring_equiv R).symm.trans $ mv_polynomial.ring_equiv_of_equiv _
id           └─────────────────────────────┘                └───────────────────────────────┘
src  ─────┘  └─────────────────────────────┘ └───────────┘ └───────────────────────────────┘└──
typ  ─────┘  └─────────────────────────────┘└───────────┘ └───────────────────────────────┘└──
doc  ─────┘  └─────────────────────────────┘ └───────────┘ └───────────────────────────────┘└──
txt  ─────┘                                  └───────────┘                                  └──
par  ─────┘                                  └───────────┘                                  └──
pid  ─────┘                                  └───────────┘                                  └──
st   ────────────────────────────────────────────────────────────────────────────────────────────
293          ⟨pempty.elim, fin.elim0, λ x, pempty.elim x, λ x, fin.elim0 x⟩) },
id                                         └─────────┘         └───────┘
src  ───────┘            └┘         └┘ └──┘└─────────┘ └┘ └──┘└───────┘ └─┘
typ  ───────┘            └┘         └┘ └──┘└─────────┘ └┘ └──┘└───────┘ └─┘
doc  ───────┘            └┘         └┘ └──┘            └┘ └──┘          └─┘
txt  ───────┘            └┘         └┘ └──┘            └┘ └──┘          └─┘
par  ───────┘            └┘         └┘ └──┘            └┘ └──┘          └─┘
pid  ───────┘            └┘         └┘ └──┘            └┘ └──┘          └┘
st   ───────────────────────────────────────────────────────────────────────┘└┘
294    exact @is_noetherian_ring_of_ring_equiv (polynomial (mv_polynomial (fin n) R)) _
id            └──────────────────────────────┘  └────────┘
src    └────┘ └──────────────────────────────┘ └────────┘                   └┘ └────
typ    └────┘ └──────────────────────────────┘ └────────┘                   └┘ └────
doc    └────┘                                  └────────┘                   └┘ └────
txt    └────┘                                                               └┘ └────
par    └────┘                                                               └┘ └────
pid                                                                        └┘ └────
st   ───────────────────────────────────────────────────────────────────────────────────
295      (mv_polynomial (fin (n+1)) R) _
id        └───────────┘            
src  ───┘ └───────────┘      └──┘ └───
typ  ───┘ └───────────┘      └──┘└───
doc  ───┘ └───────────┘       └──┘ └───
txt  ───┘                     └──┘ └───
par  ───┘                     └──┘ └───
pid  ───┘                     └──┘ └───
st   ────────────────────────────────────
296      ((mv_polynomial.option_equiv_left _ _).symm.trans (mv_polynomial.ring_equiv_of_equiv _
id         └─────────────────────────────┘                  └───────────────────────────────┘
src  ───┘  └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
typ  ───┘  └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
doc  ───┘  └─────────────────────────────┘└───────────────┘ └───────────────────────────────┘└──
txt  ───┘                                 └───────────────┘                                  └──
par  ───┘                                 └───────────────┘                                  └──
pid  ───┘                                 └───────────────┘                                  └──
st   ───────────────────────────────────────────────────────────────────────────────────────────
297        ⟨λ x, option.rec_on x 0 fin.succ, λ x, fin.cases none some x,
src  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
typ  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
doc  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
txt  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
par  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
pid  ─────┘  └──┘              └─┘        └┘ └──┘                  └─
st   ────────────────────────────────────────────────────────────────────
298        by rintro ⟨none | x⟩; [refl, exact fin.cases_succ _],
id                                            └────────────┘
src  ─────┘  └───────────────┘└─┘└──┘└──────┘└────────────┘└────
typ  ─────┘  └───────────────┘└─┘└──┘└──────┘└────────────┘└────
doc  ─────┘  └───────────────┘└─┘└──┘└──────┘              └────
txt  ─────┘  └───────────────┘└─┘└──┘└──────┘              └────
par  ─────┘  └───────────────┘└─┘└──┘└──────┘              └────
pid  ─────┘  └───────────────────────────────┘              └────
st   ───────┘└────────────────────────────────────────────────┘└─
299        λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
id                        └─┘             └───────────┘  └───────┘ └──┘ └──┘                └────┘  └─┘ 
src  ─────┘ └──┘         └─┘  └──┘     └───────────┘ └───────┘└──┘└──┘          └──┘└────┘ └─┘ └──
typ  ─────┘ └──┘         └─┘  └──┘     └───────────┘ └───────┘└──┘└──┘          └──┘└────┘ └─┘└──
doc  ─────┘ └──┘              └──┘                                              └──┘           └──
txt  ─────┘ └──┘              └──┘                                              └──┘           └──
par  ─────┘ └──┘              └──┘                                              └──┘           └──
pid  ─────┘ └──┘              └──┘                                              └──┘           └──
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────
300          0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x⟩))
id             └──────┘       └────┘            └────────────┘
src  ─────────┘└──────┘└─┘   └────┘└┘└─────┘└─┘└────────────┘└┘ └───
typ  ─────────┘└──────┘└─┘   └────┘└┘└─────┘└─┘└────────────┘└┘ └───
doc  ─────────┘        └─┘         └┘ └─────┘└─┘              └┘ └───
txt  ─────────┘        └─┘         └┘ └─────┘└─┘              └┘ └───
par  ─────────┘        └─┘         └┘ └─────┘└─┘              └┘ └───
pid  ─────────┘        └─┘         └┘ └────────┘              └┘ └───
st   ───────────────────────────────────────┘└────────────────┘└──────
301      (@@is_noetherian_ring_polynomial _ ih)
id          └───────────────────────────┘   └┘
src  ───┘   └───────────────────────────┘└─┘  └┘
typ  ───┘   └───────────────────────────┘└─┘└┘└┘
doc  ───┘   └───────────────────────────┘└─┘  └┘
txt  ───┘                                └─┘  └┘
par  ───┘                                └─┘  └┘
pid  ───┘                                └─┘  
st   ──────────────────────────────────────────┘
302  end
st   └─┘
303  
304  theorem is_noetherian_ring_mv_polynomial_of_fintype {σ : Type v} [fintype σ]
id                                                                     └─────┘ 
src                                                                    └─────┘
typ                                                                    └─────┘ 
doc                                                                    └─────┘
305    [is_noetherian_ring R] : is_noetherian_ring (mv_polynomial σ R) :=
id      └────────────────┘     └────────────────┘  └───────────┘  
src     └────────────────┘      └────────────────┘  └───────────┘
typ     └────────────────┘     └────────────────┘  └───────────┘  
doc                                                 └───────────┘
306  trunc.induction_on (fintype.equiv_fin σ) $ λ e,
id   └────────────────┘  └───────────────┘       
src  └────────────────┘  └───────────────┘
typ  └────────────────┘  └───────────────┘       
doc                      └───────────────┘
307  @is_noetherian_ring_of_ring_equiv (mv_polynomial (fin (fintype.card σ)) R) _ _ _
id    └──────────────────────────────┘  └───────────┘  └─┘  └──────────┘    
src   └──────────────────────────────┘  └───────────┘  └─┘  └──────────┘
typ   └──────────────────────────────┘  └───────────┘  └─┘  └──────────┘    
doc                                     └───────────┘       └──────────┘
308    (mv_polynomial.ring_equiv_of_equiv _ e.symm) is_noetherian_ring_mv_polynomial_fin
id      └───────────────────────────────┘   └───┘  └──────────────────────────────────┘
src     └───────────────────────────────┘    └───┘  └──────────────────────────────────┘
typ     └───────────────────────────────┘   └───┘  └──────────────────────────────────┘
doc     └───────────────────────────────┘